package ca.shojaei.mini_sat;

import java.util.*;

import org.sat4j.*;
import org.sat4j.core.*;
import org.sat4j.minisat.*;
import org.sat4j.minisat.constraints.cnf.*;
import org.sat4j.opt.*;
import org.sat4j.specs.*;

public class SAT {

	final static int MAXVAR = 1000000;
	final static int NBCLAUSES = 500000;
	
	public static boolean isSat(Vector<int[]> s)
	{
		
		
		ISolver solver = SolverFactory.newDefault ();
		// prepare the solver to accept MAXVAR variables . MANDATORY
		solver.newVar(3);
		// not mandatory for SAT solving . MANDATORY for MAXSAT solving
		solver.setExpectedNumberOfClauses(NBCLAUSES);
		
		try{
		   for(int i =0 ; i < s.size(); i++)
		   {
			   solver.addClause(new VecInt(s.get(i)));
		   }
			
			// we are done . Working now on the IProblem interface
			IProblem problem = solver ;
			if ( problem.isSatisfiable ()) {
				
				return true;
				
			}else {
			    return false; 
			}
			}catch (Exception ex)
			{
				System.out.println("Error: " + ex.getMessage());
				return false;
			}
			
	}
	
	

	public static void printVec(Vector<int[]> v)
	{
		for(int i = 0 ; i < v.size(); i++)
		{
			int[] temp = v.get(i);
			for(int j = 0; j < temp.length ; j++)
				System.out.print(temp[j] + " ");
			
			System.out.println();
		}
	}
	
	public static Vector<int[]> clean(Vector<int[]> v)
	{
		Vector<int[]> result = new Vector<int[]>(v.size());
		
		for(int i = 0 ; i < v.size();i++){
			if(!result.contains(v.get(i)))
				result.add(v.get(i));
					
		}
		
		return result;
	}
	
	
	public static boolean contain(Vector<int[]> v, int[] c)
	{
		for(int i = 0 ; i < v.size(); i++)
		{
			if(Arrays.equals(v.get(i), c))
				return true;
		}
		
		return false;
	}

}
